Boehm-Berarducci Encoding

Boehm-Berarducci encoding is often confused with Church encoding. First of all, Church encoding, which represents data types in an untyped lambda-calculus, is not tight. Without types, it is impossible to separate lambda-terms that encode some data type, from the terms that represent no value of that data type. The main distinction between the two approaches is subtle. In a word, Church encoding only describes introductions whereas Boehm and Berarducci also define the elimination, or pattern-matching, on encoded data types.

Boehm-Berarducci Encodingはeliminationも定義している

code:hs

-- 2つの関数を引数に取る

type BBEither a b = forall r. (a -> r) -> (b -> r) -> r

-- left, rightのコンストラクタ

left :: a -> BBEither a b

left x = \f g -> f x

right :: b -> BBEither a b

right x = \f g -> g x

-- Either a bに対するパターンマッチを行う関数

either' :: (a -> r) -> (b -> r) -> BBEither a b -> r

either' f g e = e f g

code:hs

import Prelude hiding (Either, Left, Right)

main :: IO ()

main = do

let a = left 42

let b = right "hello"

let resultA = either' show id a

let resultB = either' show id b

putStrLn $ "Result A: " ++ resultA

putStrLn $ "Result B: " ++ resultB